Skip to content

STL frontend: expr2stl conversion #4954

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 2 commits into from
Jul 31, 2019
Merged

STL frontend: expr2stl conversion #4954

merged 2 commits into from
Jul 31, 2019

Conversation

MatWise
Copy link
Contributor

@MatWise MatWise commented Jul 26, 2019

Expands the expr2statement_list stub and adds suport for the conversion of the following expressions:

  • and
  • or
  • xor
  • not
  • equal
  • unequal

Also adds support for the STL NOT instruction.
Note that this hardly changes any output of CBMC itself since any instruction not listed here will redirect to expr2c. Therefore this is only relevant to projects that rely on CBMC, use the STL language interface and want to convert pure boolean expressions.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@MatWise
Add support for STL NOT instruction
ae6dd2f 
Extends the language subset of Statement List by the NOT instruction,
used for simply negating the current state of the rlo.
allredj
allredj reviewed Jul 26, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: ce56308).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120871525

@codecov-io
Copy link

codecov-io commented Jul 26, 2019 •
edited
Loading

Codecov Report

Merging #4954 into develop will decrease coverage by 0.1%.
The diff coverage is 1.75%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #4954      +/-   ##
===========================================
- Coverage    69.29%   69.19%   -0.11%     
===========================================
  Files         1306     1308       +2     
  Lines       108263   108206      -57     
===========================================
- Hits         75023    74868     -155     
- Misses       33240    33338      +98
Impacted Files Coverage Δ
src/statement-list/statement_list_typecheck.h 100% <ø> (ø) ⬆️
...rc/statement-list/converters/expr2statement_list.h 0% <0%> (ø)
.../statement-list/converters/expr2statement_list.cpp 0% <0%> (ø) ⬆️
src/statement-list/scanner.l 76.55% <100%> (+0.11%) ⬆️
src/statement-list/statement_list_typecheck.cpp 73.39% <11.11%> (-0.94%) ⬇️
...olvers/strings/string_constraint_instantiation.cpp 90.1% <0%> (-3.3%) ⬇️
src/util/format_expr.cpp 72.18% <0%> (-3.01%) ⬇️
src/goto-symex/renaming_level.cpp 92.53% <0%> (-2.52%) ⬇️
src/cpp/cpp_declarator_converter.cpp 76.06% <0%> (-0.99%) ⬇️
jbmc/src/java_bytecode/java_bytecode_parser.cpp 89.59% <0%> (-0.98%) ⬇️
... and 48 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 9643ec2...f84bf71. Read the comment docs.

pkesseli
pkesseli suggested changes Jul 27, 2019
View reviewed changes
@MatWise MatWise force-pushed the feature/stl-from-expression branch 2 times, most recently from 3208859 to 7c73b95 Compare July 29, 2019 15:19
allredj
allredj reviewed Jul 29, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 3208859).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121117967
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj
allredj reviewed Jul 29, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: 7c73b95).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121120142

pkesseli
pkesseli suggested changes Jul 30, 2019
View reviewed changes
@MatWise
Expand expr2statement_list
f84bf71 
Adds support for the conversion of boolean expressions. Note that this
will hardly have any effect on the output of CBMC and in the current
state only be used by projects which rely on it.

There are several STL-specific simplification routines integrated in the
conversion, e.g. changing the conversion order of operands to avoid
unnecessary nesting.
@MatWise MatWise force-pushed the feature/stl-from-expression branch from 7c73b95 to f84bf71 Compare July 30, 2019 16:01
allredj
allredj reviewed Jul 30, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✔️
Passed Diffblue compatibility checks (cbmc commit: f84bf71).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/121286487

@pkesseli pkesseli merged commit c494b9c into diffblue:develop Jul 31, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@pkesseli pkesseli pkesseli approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@tautschnig tautschnig Awaiting requested review from tautschnig tautschnig is a code owner

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@MatWise @codecov-io @pkesseli @allredj